(DEFPROP FNS (FNS FF) VALUE) (DEFPROP FF (LAMBDA(N) (COND ((EQUAL N 1.) 0.) ((ZEROP (REMAINDER N 2.)) (ADD1 (FF (QUOTIENT N 2.)))) (T (ADD1 (FF (QUOTIENT (ADD1 (TIMES 3. N)) 2.)))))) EXPR)